Nuprl Lemma : f2f+-pred-field 11,40

es:ES, ff:FIFO, f2f+:F2F+-decls, sndrrcvr:ff.C, ee':E.
f2f+-pred(e',e)
 {([esndr is_req   rcvr [ercvr is_ack  sndr])
 & ([e'sndr is_req   rcvr [e'rcvr is_ack  sndr])} 
latex


Definitionsis_ack , [ei p j], is_req  , left + right, P  Q, x:AB(x), f2f+-pred(e',e), P & Q, ES, t  T, FIFO, F2F+-decls, ff.C, E, P  Q, {T}, x:AB(x), x:A  B(x), f(a), ff.S, , s = t, s ~ t, SQType(T), let x,y = A in B(x;y), t.1, [ei p j]
LemmasfifoS wf, f2f+Ack wf, snd-it wf, f2f+Req wf, f2f+-pred wf, es-E wf, fifoC wf, F2F+-decls wf, FIFO wf, event system wf, f2f+-property

origin